COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	setops[f85,jmc]		Proofs of properties of set operations in EKL
C00003 ENDMK
C⊗;
setops[f85,jmc]		Proofs of properties of set operations in EKL

;;; We have EKL definitions corresponding to the Lisp definitions
;;; of the Fall 1985 take home final.
;;; We also define functions ground→(ground→truthval) taking a Lisp
;;; list into the predicate of membership in the list.
;;; We then prove that the Lisp functions union and intersection
;;; operating on the list representations of sets correspond to
;;; the union and intersection operations on the predicates.
;;; This makes it easy to prove the algebraic properties of the
;;; Lisp functions.